es:ES, ff:FIFO, i:ff.C, e:{e:E| ff.R(i,e)} . (ff.Sender(i,e) < e) 

latex

Definitions	x:A. B(x), t  T, , Q  f P, P & Q, Q f P, A c B
Lemmas	es-E wf, fifoR wf, fifoC wf, FIFO wf, event system wf, fifoSender-antecedent